\begin{tabbing}
MsgA
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type\+
\\[0ex]$\times$ (${\it da}$:$a$:Knd fp$\rightarrow$ Type
\\[0ex]$\times$ ${\it init}$:$x$:Id fp$\rightarrow$ $\mathbb{Q}\rightarrow$${\it ds}$($x$)?Void
\\[0ex]$\times$ ${\it pre}$:$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow\mathbb{B}$
\\[0ex]$\times$ ${\it ef}$:${\it kx}$::Knd $\times$ Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kx}$.1)$\rightarrow\mathbb{Q}\rightarrow$${\it ds}$(${\it kx}$.2)?Void
\\[0ex]$\times$ ${\it send}$:\=${\it kl}$::Knd $\times$ IdLnk fp$\rightarrow$\+
\\[0ex](${\it tg}$:Id $\times$ (State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kl}$.1)$\rightarrow$(${\it da}$(rcv(${\it kl}$.2,${\it tg}$))?Void List))) List
\-\\[0ex]$\times$ ${\it frame}$:$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ ${\it sframe}$:${\it ltg}$::IdLnk $\times$ Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ ${\it aframe}$:$k$:Knd fp$\rightarrow$ Id List
\\[0ex]$\times$ ${\it bframe}$:$k$:Knd fp$\rightarrow$ IdLnk List
\\[0ex]$\times$ ${\it rframe}$:$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ (${\it prob}$:$a$:Id fp$\rightarrow$ FinProbSpace
\\[0ex]$\times$ Top))
\-
\end{tabbing}